/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.Iterator;

import alloy.ast.ArrowMultExpr;
import alloy.ast.ComprehensionExpr;
import alloy.ast.LeafId;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Variable;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.PermIter;

/** Iterates over the possible values of a quantified {@link Variable}.  For each value,
    yields {@link BoolSwitch} value representing that value of the {@link Variable}.
    Takes into account the variable's {@link RelationType} and the
    set or relation multiplicity constraints.
    <p>
    This iterator encapsulates the correspondence between {@link BoolSwitch} values and
    the values of the quantified variables.
    <p>
    API: call {@link #makeIterator} or {@link #makeSingleTupleIterator} to get the {@link Iterator}
    you want.
    <p>
    @see BooleanFormula#makeSwitch
    @see BooleanFormula#makeSwitchableConst
*/
public abstract class VariableValueIterator implements Iterator {
    /** The current {@link BoolSwitch} value, representing the last yielded
	relational value of the quantified {@link Variable}. */
    protected long _boolSwitchValue;

    /**
     * {@link RelationType} of the quantified variable over whose
     * values we're iterating.
     */
    private RelationType _relType;

    /** For each dimension, the size of the flat array block dedicated to one
	unit of that dimension.  Equal to the product of values of subsequent
	dimensions. */
    private int[] _dimSize;

    //
    // Methods
    //

    protected VariableValueIterator(RelationType relType_) {
	_relType = relType_;
	_dimSize = new int[relType_.arity()];
	int flatSize = 1;
	int dsize = 1; 
	for (int i=relType_.arity()-1; i>=0; i--) {
	    _dimSize[i] = dsize;
	    int scope = relType_.getBasicTypeAt(i).getScope();
	    dsize *= scope;
	    flatSize *= scope;
	}
	Dbg.chk(flatSize <= 64);
    }  // VariableValueIterator()

    /**
     * Compute the index of the bit in {@link #_boolSwitchValue}
     * representing the tuple with the given coordinates (indices).
     * This routine encapsulates the correspondence between
     * relation tuples and bits of the {@link BoolSwitch}.
     * @see alloy.util.MultiDimArray#_inds2flat
     */
    protected int getBitForTuple(int[] tupleInds_) {
	int flatInd = 0;
	for (int i=0; i<tupleInds_.length; i++)
	    flatInd += (tupleInds_[i] * _dimSize[i]);
	return flatInd;
    }

    protected void setTuple(int[] tupleInds_) {
	_boolSwitchValue |= (1 << getBitForTuple(tupleInds_));
    }

    /**
     * Create an {@link Iterator} which yields the possible values of a quantified
     * {@link Variable} given its {@link LeafId} and the {@link TranslInfo translator}
     * used to translate the Alloy {@link alloy.ast.Formula}.
     */
    public static Iterator makeIterator(LeafId quantVarLeafId_,
					TranslInfo translator_) {
	RelationType relType = translator_.getLeafType(quantVarLeafId_);
	MultiplicityExpr mult = translator_.getLeafMultiplicity(quantVarLeafId_);
	boolean declaredInComprehension = translator_.getVarCreator(quantVarLeafId_) instanceof ComprehensionExpr;
	return makeIterator(relType, mult, declaredInComprehension);
    }

    /**
     * Create an {@link Iterator} which yields the possible values of a quantified
     * {@link Variable} given its {@link RelationType} and {@link MultiplicityExpr multiplicity}.
     */
    public static Iterator makeIterator(RelationType relType_,
					MultiplicityExpr multExpr_,
					boolean declaredInComprehension_) {
	if (declaredInComprehension_)
	    return makeSingleTupleIterator(relType_, false /* don't include empty relation */);
	
	// determine the kind of iterator based on the multiplicity.
	if (relType_.arity() == 1) {
	    Multiplicity mult = multExpr_.getMult();
	    if (mult.equals(Multiplicity.NONE) || mult.equals(Multiplicity.ONE)) {
		    return makeSingleTupleIterator(relType_, false /* don't include empty relation */);
	    } else if (mult.equals(Multiplicity.LONE)) {
	        return makeSingleTupleIterator(relType_, true /* include empty relation */);
	    } else if (mult.equals(Multiplicity.SET)) {
	        return new AllValuesIterator(relType_);
	    } else {
	        return null;
	    }
	} else {
	    // for relation-valued quantified variables,
	    // temporarily, return ALL values, ignoring the multiplicities,
	    // unless the relation is a permutation.

            // we still need to check if multExpr_ is an ArrowMultExpr,
            // since SetMultExprs can have relation types of arity > 1
            if (multExpr_ instanceof ArrowMultExpr) {
                ArrowMultExpr arrowMult = (ArrowMultExpr)multExpr_;
                Multiplicity leftMult = arrowMult.getLeft().getMult();
                Multiplicity rightMult = arrowMult.getRight().getMult();
                if (leftMult.equals(Multiplicity.ONE) &&
                    rightMult.equals(Multiplicity.ONE))
                    return new PermutationIterator(relType_);
            }
            return new AllValuesIterator(relType_);
	}
    }
    
    /** Create an {@link Iterator} which yields all single-tuple values of a quantified
	{@link Variable}, plus possibly the empty-relation value.  */
    public static Iterator makeSingleTupleIterator(RelationType relType_,
						   boolean includeEmptyRelation_) {
	return new SingleTupleIterator(relType_, includeEmptyRelation_);
    }
    
    /** @return the {@link Long} {@link BoolSwitch} value corresponding to the next quantified variable. */
    public abstract Object next();
    public abstract boolean hasNext();
    
    /** Remove not supported -- this is a read-only iterator. */
    public void remove() throws UnsupportedOperationException
    { throw new UnsupportedOperationException("DeclIter.remove()"); }

    //
    // Iterator implementations for specific cases
    //
    
    /** A {@link VariableValueIterator} that yields <em>singleton</em> values of a relations,
	i.e. all values containing exactly one tuple, plus possibly the empty relation. */
    private static class SingleTupleIterator extends VariableValueIterator {
	/** Number of values left to return */
	private int _leftToReturn;
	
	SingleTupleIterator(RelationType relType_, boolean includeEmptyRelation_) {
	    super(relType_);
	    _boolSwitchValue = includeEmptyRelation_ ? 0 : 1;
	    // compute the # of values to return.  this is the number of bits
	    // in the relation, plus one if includeEmptyRelation_
	    _leftToReturn = 1;
	    for (int i=0; i<relType_.arity(); i++)
		_leftToReturn *= relType_.getBasicTypeAt(i).getScope();
	    if (includeEmptyRelation_)
		_leftToReturn++;
	}
	
	public Object next() {
	    Long curValue = new Long(_boolSwitchValue);
	    if (_boolSwitchValue == 0)
		_boolSwitchValue = 1;
	    else {
		_boolSwitchValue = (_boolSwitchValue << 1);
		Dbg.chk(_boolSwitchValue > 0);
	    }
	    _leftToReturn--;
	    return curValue;
	}

	public boolean hasNext() { return _leftToReturn > 0; }
    }  // class SingleTupleIterator

    /** A {@link VariableValueIterator} which yields <em>all</em> possible values
	of a quantified {@link Variable} of a given type.  Multiplicities can then
	be used to filter out values that are ruled out (e.g. not funtions).
	For an m x n relation that's 2^(m*n) values. */
    private static class AllValuesIterator extends VariableValueIterator {
	/** Number of values still to be returned. */
	private long _leftToReturn;
	
	AllValuesIterator(RelationType relType_) {
	    super(relType_);
	    // compute _leftToReturn
	    _leftToReturn = 1;
	    for (int i=0; i<relType_.arity(); i++)
		_leftToReturn *= relType_.getBasicTypeAt(i).getScope();
	    _leftToReturn = (1 << _leftToReturn);
	    Dbg.chk(_leftToReturn > 0);
	}

	public Object next() {
	    Long curVal = new Long(_boolSwitchValue++);
	    _leftToReturn--;
	    return curVal;
	}
	public boolean hasNext() { return _leftToReturn > 0; }
    }  // class VariableValueIterator.AllValuesIterator

    /**
     * A {@link VariableValueIterator} which yields all values of a
     * permutation, i.e. of a homogeneous binary relation declared
     * with multiplicity !->!.
     */
    private static class PermutationIterator extends VariableValueIterator {
	/** Iterator over the permutations. */
	private PermIter _permIter;

	PermutationIterator(RelationType relType_) {
	    super(relType_);
	    Dbg.chk(relType_.arity() == 2 &&
		    relType_.getBasicTypeAt(0).equals(relType_.getBasicTypeAt(1)));
	    _permIter = new PermIter(relType_.getBasicTypeAt(0).getScope());
	}

	public Object next() {
	    int[] perm = (int[])_permIter.next();
	    _boolSwitchValue = 0;
	    for (int i=0; i<perm.length; i++)
		setTuple(new int[]{i, perm[i]});
	    return new Long(_boolSwitchValue);
	}

	public boolean hasNext() { return _permIter.hasNext(); }
    }
    
}  // class VariableValueIterator





    
